Issue1441.agda:13,3-7
Set₂ is not less or equal than Set₁
when checking that the type
(A : Type) → (A → ∃ Tree') → Tree' (Box A) of the constructor sup'
fits in the sort Set₁ of the datatype.
